COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	GRUMBLES ABOUT CGOL
C00010 ENDMK
C⊗;
GRUMBLES ABOUT CGOL


	These grumbles about CGOL are from the following point of view:

	1. Lisp functions are mathematical entities definable by
mathematical equations in which substitutivity of equals by equals
holds.  Cartwright has shown how to make this interpretation stick
for pure Lisp.

	2. Besides pure Lisp, the working versions have many other
features.  I regard the notation for these features as rather bad
and subject to revision in spite of the many years these notations
have persisted.  Any kind of M-expression notation should make the
pure Lisp come out elegantly and the rest come out merely conveniently.

	3. My present idea is that an on-line system should accept
assertions, questions, and commands and these may require notational
distinction.  At present Lisp treats them all as questions.  Thus
when a user types (car '(a b)), he is asking Lisp the value of this
expression, and the system straightforwardly says  A.  Other requests
are forced into this format as is seen by the fact that what is typed
in response to them is often arbitrary, as in the case of DEFINE, or
redundant as in the case of PRINT.

	A Lisp function definition should be regarded as an assertion,
and therefore should be written as a sentence in some language.  One
can imagine combining such assertions with propositional and
predicate logic to make compound assertions if that should be useful.
This view has the consequence that the top level of the function
definition should have some logical form.

	Measuring CGOL against these criteria leads to some grumbles.
Suppose we define the function ALT by

DEFINE "ALT" X,13; IF NULL X OR NULL CDR X THEN X ELSE CAR X . ALT CDDR X$.

	1. I have no complaint at all about the right hand side from IF
up to but not including <alt mode>.

	2. The binding power is a different kind of information
and should be given separately before or after (at the user's option)
the semantic definition.  Can this be done?

	3. From the first order logic point of view "ALT" is strange.
Without a logical explanation, it is unacceptable.  Single quote would
be just as unacceptable.

	4. The semicolon as a relation of equality or operator of
assignment is ugly.

	5. \ for λ is ugly.  I trust λ is acceptable.  A word would
be better in alphabets without λ.

	6. The <alt mode> termination seems ugly, because it isn't suitable
for inclusion in files.  It is allowable provided it is regarded as
an abbreviation for a terminator like . followed by an activation command.

	Given these criticisms, I would prefer something like

ALT = mu(alt,∀X. alt X = IF NULL X OR NULL CDR X THEN X ELSE CAR X . alt CDDR X).

perhaps contractible to

ALT X ← IF NULL X OR NULL CDR X THEN X ELSE CAR X . ALT CDDR X.

where the ← signals that the statement is an assertion and that it
asserts a recursive function definition.
Here we are assuming that the syntactic use of ALT as a prefix operator
has either been asserted previously or is an assumed property of single
argument functions.  If we wished to do this later, the arguments of
ALT would be parenthesized on both sides.

	The above is an assertion that ALT is the least alt satisfying
the condition.  In principle, when it receives this information, the
system should do nothing beyond what is required to verify its understanding
of the definition, complaining if it doesn't understand.

	According to our present understanding, the definition should then
make available the Cartwright sentence

	∀X.ALT X = IF NULL X OR NULL CDR X THEN X ELSE CAR X . ALT CDDR X

and the axiom schema

	∀X. IS-SEXP(IF NULL X OR NULL CDR X THEN X ELSE CAR X . G(CDR X))
⊃ G(X) = IF NULL X OR NULL CDR X THEN X ELSE CAR X . G(CDR X)) ⊃
(∀X.(IS-SEXP ALT X) ⊃ G(X) = ALT X)

where G is a free function variable.  These formulas are then available
for proving facts about the function just defined.

	On the computational level, the assertion should also make
available to the interpreter or compiler the ability to compute ALT
applied to arguments.

	A system that has all these desired properties doesn't yet
exist, and maybe creating it should await some further ideas on how
to get rid of the anomalies in the non-pure part of Lisp as well as
some experience in determining whether the first order characterization
of Lisp functions is just the thing.

	For the present, I am reluctant to use CGOL for CS206 in the
Spring, because the notation of function definition seems a hack and
misleading from the above point of view.